Left Termination proof of /tmp/tmp2TDZXN/gopher2.pl

Left Termination of the query pattern
gopher(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇒, 185 ms)

↳2 Prolog

↳3 PrologToPiTRSProof (⇒, 0 ms)

↳4 PiTRS

↳5 DependencyPairsProof (⇔, 15 ms)

↳6 PiDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 TRUE

(0) Obligation:

Clauses:

gopher(nil, nil).
gopher(X, cons(nil, T)) :- ','(no(empty(X)), ','(head(X, nil), tail(X, T))).
gopher(X, Y) :- ','(no(empty(X)), ','(head(X, H), ','(no(empty(H)), ','(head(H, U), ','(tail(H, V), ','(tail(X, W), gopher(cons(U, cons(V, W)), Y))))))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, X), X).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: gopher(g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: gopher(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: gopher(T1, T2), SCOPE: 1, CLAUSE: 0 | gopher(T1, T2), SCOPE: 1, CLAUSE: 1 | gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | gopher(nil, T2), SCOPE: 1, CLAUSE: 1 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: gopher(T1, T2), SCOPE: 1, CLAUSE: 1 | gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\ngopher(T1, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: gopher(nil, T2), SCOPE: 1, CLAUSE: 1 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))) | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\nX7 is free\nX8 is free\ngopher(nil, T2) !=? gopher(X7, cons(nil, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 8 | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(','(call(empty(nil)), ','(!_2, failure(a))), ','(head(nil, nil), tail(nil, T5))) | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(empty(nil), ','(','(!_2, failure(a)), ','(head(nil, nil), tail(nil, T5)))) | ?_3 | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(empty(nil), ','(','(!_2, failure(a)), ','(head(nil, nil), tail(nil, T5)))), SCOPE: 4, CLAUSE: 7 | ?_4 | ?_3 | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ?_4 | ?_3 | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ?_3 | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(head(nil, nil), tail(nil, T5))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(head(nil, nil), tail(nil, T5)), SCOPE: 5, CLAUSE: 3 | ','(head(nil, nil), tail(nil, T5)), SCOPE: 5, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(head(nil, nil), tail(nil, T5)), SCOPE: 5, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))))\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 8 | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(','(call(empty(nil)), ','(!_6, failure(a))), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))) | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(empty(nil), ','(','(!_6, failure(a)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))))) | ?_7 | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(empty(nil), ','(','(!_6, failure(a)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))))), SCOPE: 8, CLAUSE: 7 | ?_8 | ?_7 | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ?_8 | ?_7 | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ?_7 | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))), SCOPE: 9, CLAUSE: 3 | ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))), SCOPE: 9, CLAUSE: 4\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))), SCOPE: 9, CLAUSE: 4\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))))\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 8 | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(','(call(empty(nil)), ','(!_10, failure(a))), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))) | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(empty(nil), ','(','(!_10, failure(a)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))))) | ?_11 | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(empty(nil), ','(','(!_10, failure(a)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))))), SCOPE: 12, CLAUSE: 7 | ?_12 | ?_11 | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ?_12 | ?_11 | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ?_11 | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))), SCOPE: 13, CLAUSE: 3 | ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))), SCOPE: 13, CLAUSE: 4\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))), SCOPE: 13, CLAUSE: 4\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(no(empty(T16)), ','(head(T16, nil), tail(T16, T18))) | gopher(T16, T2), SCOPE: 1, CLAUSE: 2\n\nT16 is ground\ngopher(T16, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX62 is free\nX63 is free\ngopher(T1, T2) !=? gopher(nil, nil)\ngopher(T1, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(no(empty(T16)), ','(head(T16, nil), tail(T16, T18))), SCOPE: 14, CLAUSE: 8 | ','(no(empty(T16)), ','(head(T16, nil), tail(T16, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T16, T2), SCOPE: 1, CLAUSE: 2\n\nT16 is ground\ngopher(T16, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(','(call(empty(T21)), ','(!_14, failure(a))), ','(head(T21, nil), tail(T21, T18))) | ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(empty(T21), ','(','(!_14, failure(a)), ','(head(T21, nil), tail(T21, T18)))) | ?_15 | ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(empty(T21), ','(','(!_14, failure(a)), ','(head(T21, nil), tail(T21, T18)))), SCOPE: 16, CLAUSE: 7 | ?_16 | ?_15 | ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(','(!_14, failure(a)), ','(head([], nil), tail([], T18))) | ?_16 | ?_15 | ','(no(empty([])), ','(head([], nil), tail([], T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ?_16 | ?_15 | ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(failure(a), ','(head([], nil), tail([], T18))) | gopher([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(failure(a), ','(head([], nil), tail([], T18)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: gopher([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(failure(a), ','(head([], nil), tail([], T18))), SCOPE: 17, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26)))))))\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 8 | ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 9\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(','(call(empty([])), ','(!_18, failure(a))), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))) | ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 9\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(empty([]), ','(','(!_18, failure(a)), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26)))))))) | ?_19 | ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 9\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(empty([]), ','(','(!_18, failure(a)), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26)))))))), SCOPE: 20, CLAUSE: 7 | ?_20 | ?_19 | ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 9\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(','(!_18, failure(a)), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))) | ?_20 | ?_19 | ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 9\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(failure(a), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26)))))))\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(failure(a), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 21, CLAUSE: 10\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ?_15 | ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(head(T31, nil), tail(T31, T18))\n\nT31 is ground\ngopher(T31, T2) !=? gopher(nil, nil)\nempty(T31) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(head(T31, nil), tail(T31, T18)), SCOPE: 22, CLAUSE: 3 | ','(head(T31, nil), tail(T31, T18)), SCOPE: 22, CLAUSE: 4\n\nT31 is ground\ngopher(T31, T2) !=? gopher(nil, nil)\nempty(T31) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(head(T31, nil), tail(T31, T18)), SCOPE: 22, CLAUSE: 4\n\nT31 is ground\ngopher(T31, T2) !=? gopher(nil, nil)\nempty(T31) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: tail(.(nil, T37), T18)\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: tail(.(nil, T37), T18), SCOPE: 23, CLAUSE: 5 | tail(.(nil, T37), T18), SCOPE: 23, CLAUSE: 6\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: tail(.(nil, T37), T18), SCOPE: 23, CLAUSE: 6\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(no(empty(T46)), ','(head(T46, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T46, X115), gopher(cons(X113, cons(X114, X115)), T48)))))))\n\nT46 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T46, T2) !=? gopher(nil, nil)\nempty(T46) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(no(empty(T46)), ','(head(T46, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T46, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 8 | ','(no(empty(T46)), ','(head(T46, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T46, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT46 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T46, T2) !=? gopher(nil, nil)\nempty(T46) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(','(call(empty(T51)), ','(!_24, failure(a))), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))) | ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(empty(T51), ','(','(!_24, failure(a)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48)))))))) | ?_25 | ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(empty(T51), ','(','(!_24, failure(a)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48)))))))), SCOPE: 26, CLAUSE: 7 | ?_26 | ?_25 | ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ?_26 | ?_25 | ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ?_25 | ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(head(T54, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T54, X115), gopher(cons(X113, cons(X114, X115)), T48))))))\n\nT54 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T54, T2) !=? gopher(nil, nil)\nempty(T54) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(head(T54, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T54, X115), gopher(cons(X113, cons(X114, X115)), T48)))))), SCOPE: 27, CLAUSE: 3 | ','(head(T54, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T54, X115), gopher(cons(X113, cons(X114, X115)), T48)))))), SCOPE: 27, CLAUSE: 4\n\nT54 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T54, T2) !=? gopher(nil, nil)\nempty(T54) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(head(T54, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T54, X115), gopher(cons(X113, cons(X114, X115)), T48)))))), SCOPE: 27, CLAUSE: 4\n\nT54 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T54, T2) !=? gopher(nil, nil)\nempty(T54) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(no(empty(T59)), ','(head(T59, X113), ','(tail(T59, X114), ','(tail(.(T59, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))))\n\nT59 is ground\nT60 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(no(empty(T59)), ','(head(T59, X113), ','(tail(T59, X114), ','(tail(.(T59, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 8 | ','(no(empty(T59)), ','(head(T59, X113), ','(tail(T59, X114), ','(tail(.(T59, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT59 is ground\nT60 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(','(call(empty(T63)), ','(!_28, failure(a))), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))) | ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(empty(T63), ','(','(!_28, failure(a)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))))) | ?_29 | ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(empty(T63), ','(','(!_28, failure(a)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))))), SCOPE: 30, CLAUSE: 7 | ?_30 | ?_29 | ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(','(!_28, failure(a)), ','(head([], X113), ','(tail([], X114), ','(tail(.([], T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))) | ?_30 | ?_29 | ','(no(empty([])), ','(head([], X113), ','(tail([], X114), ','(tail(.([], T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ?_30 | ?_29 | ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T63) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(failure(a), ','(head([], X113), ','(tail([], X114), ','(tail(.([], T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))))\n\nT60 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(failure(a), ','(head([], X113), ','(tail([], X114), ','(tail(.([], T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 31, CLAUSE: 10\n\nT60 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ?_29 | ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T63) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T63) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(head(T66, X113), ','(tail(T66, X114), ','(tail(.(T66, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))\n\nT60 is ground\nT66 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T66) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(head(T66, X113), ','(tail(T66, X114), ','(tail(.(T66, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))), SCOPE: 32, CLAUSE: 3 | ','(head(T66, X113), ','(tail(T66, X114), ','(tail(.(T66, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))), SCOPE: 32, CLAUSE: 4\n\nT60 is ground\nT66 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T66) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(head(T66, X113), ','(tail(T66, X114), ','(tail(.(T66, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))), SCOPE: 32, CLAUSE: 4\n\nT60 is ground\nT66 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T66) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(tail(.(T71, T72), X114), ','(tail(.(.(T71, T72), T60), X115), gopher(cons(T71, cons(X114, X115)), T48)))\n\nT60 is ground\nT71 is ground\nT72 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(tail(.(T71, T72), X114), ','(tail(.(.(T71, T72), T60), X115), gopher(cons(T71, cons(X114, X115)), T48))), SCOPE: 33, CLAUSE: 5 | ','(tail(.(T71, T72), X114), ','(tail(.(.(T71, T72), T60), X115), gopher(cons(T71, cons(X114, X115)), T48))), SCOPE: 33, CLAUSE: 6\n\nT60 is ground\nT71 is ground\nT72 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(tail(.(T71, T72), X114), ','(tail(.(.(T71, T72), T60), X115), gopher(cons(T71, cons(X114, X115)), T48))), SCOPE: 33, CLAUSE: 6\n\nT60 is ground\nT71 is ground\nT72 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(tail(.(.(T77, T78), T60), X115), gopher(cons(T77, cons(T78, X115)), T48))\n\nT60 is ground\nT77 is ground\nT78 is ground\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(tail(.(.(T77, T78), T60), X115), gopher(cons(T77, cons(T78, X115)), T48)), SCOPE: 34, CLAUSE: 5 | ','(tail(.(.(T77, T78), T60), X115), gopher(cons(T77, cons(T78, X115)), T48)), SCOPE: 34, CLAUSE: 6\n\nT60 is ground\nT77 is ground\nT78 is ground\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(tail(.(.(T77, T78), T60), X115), gopher(cons(T77, cons(T78, X115)), T48)), SCOPE: 34, CLAUSE: 6\n\nT60 is ground\nT77 is ground\nT78 is ground\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: gopher(cons(T85, cons(T86, T87)), T48)\n\nT85 is ground\nT86 is ground\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(no(empty(T90)), ','(head(T90, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T90, X163), gopher(cons(X161, cons(X162, X163)), T92)))))))\n\nT90 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T90, T2) !=? gopher(nil, nil)\ngopher(T90, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(no(empty(T90)), ','(head(T90, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T90, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 8 | ','(no(empty(T90)), ','(head(T90, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T90, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT90 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T90, T2) !=? gopher(nil, nil)\ngopher(T90, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(','(call(empty(T95)), ','(!_35, failure(a))), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))) | ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(empty(T95), ','(','(!_35, failure(a)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92)))))))) | ?_36 | ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(empty(T95), ','(','(!_35, failure(a)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92)))))))), SCOPE: 37, CLAUSE: 7 | ?_37 | ?_36 | ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(','(!_35, failure(a)), ','(head([], X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail([], X163), gopher(cons(X161, cons(X162, X163)), T92))))))) | ?_37 | ?_36 | ','(no(empty([])), ','(head([], X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail([], X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nX160 is free\nX161 is free\nX162 is free\nX163 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ?_37 | ?_36 | ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))\nempty(T95) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(failure(a), ','(head([], X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail([], X163), gopher(cons(X161, cons(X162, X163)), T92)))))))\n\nX160 is free\nX161 is free\nX162 is free\nX163 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(failure(a), ','(head([], X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail([], X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 38, CLAUSE: 10\n\nX160 is free\nX161 is free\nX162 is free\nX163 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ?_36 | ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))\nempty(T95) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))\nempty(T95) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(head(T98, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T98, X163), gopher(cons(X161, cons(X162, X163)), T92))))))\n\nT98 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T98, T2) !=? gopher(nil, nil)\ngopher(T98, T2) !=? gopher(X62, cons(nil, X63))\nempty(T98) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(head(T98, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T98, X163), gopher(cons(X161, cons(X162, X163)), T92)))))), SCOPE: 39, CLAUSE: 3 | ','(head(T98, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T98, X163), gopher(cons(X161, cons(X162, X163)), T92)))))), SCOPE: 39, CLAUSE: 4\n\nT98 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T98, T2) !=? gopher(nil, nil)\ngopher(T98, T2) !=? gopher(X62, cons(nil, X63))\nempty(T98) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(head(T98, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T98, X163), gopher(cons(X161, cons(X162, X163)), T92)))))), SCOPE: 39, CLAUSE: 4\n\nT98 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T98, T2) !=? gopher(nil, nil)\ngopher(T98, T2) !=? gopher(X62, cons(nil, X63))\nempty(T98) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(no(empty(T103)), ','(head(T103, X161), ','(tail(T103, X162), ','(tail(.(T103, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))))\n\nT103 is ground\nT104 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T103, T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(no(empty(T103)), ','(head(T103, X161), ','(tail(T103, X162), ','(tail(.(T103, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 8 | ','(no(empty(T103)), ','(head(T103, X161), ','(tail(T103, X162), ','(tail(.(T103, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT103 is ground\nT104 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T103, T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(','(call(empty(T107)), ','(!_40, failure(a))), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))) | ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(empty(T107), ','(','(!_40, failure(a)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))))) | ?_41 | ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(empty(T107), ','(','(!_40, failure(a)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))))), SCOPE: 42, CLAUSE: 7 | ?_42 | ?_41 | ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(','(!_40, failure(a)), ','(head([], X161), ','(tail([], X162), ','(tail(.([], T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))) | ?_42 | ?_41 | ','(no(empty([])), ','(head([], X161), ','(tail([], X162), ','(tail(.([], T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.([], T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ?_42 | ?_41 | ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T107) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(failure(a), ','(head([], X161), ','(tail([], X162), ','(tail(.([], T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))))\n\nT104 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.([], T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(failure(a), ','(head([], X161), ','(tail([], X162), ','(tail(.([], T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 43, CLAUSE: 10\n\nT104 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.([], T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ?_41 | ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T107) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T107) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(head(T110, X161), ','(tail(T110, X162), ','(tail(.(T110, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))\n\nT104 is ground\nT110 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T110, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T110) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(head(T110, X161), ','(tail(T110, X162), ','(tail(.(T110, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))), SCOPE: 44, CLAUSE: 3 | ','(head(T110, X161), ','(tail(T110, X162), ','(tail(.(T110, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))), SCOPE: 44, CLAUSE: 4\n\nT104 is ground\nT110 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T110, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T110) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(head(T110, X161), ','(tail(T110, X162), ','(tail(.(T110, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))), SCOPE: 44, CLAUSE: 4\n\nT104 is ground\nT110 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T110, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T110) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(tail(.(T115, T116), X162), ','(tail(.(.(T115, T116), T104), X163), gopher(cons(T115, cons(X162, X163)), T92)))\n\nT104 is ground\nT115 is ground\nT116 is ground\nX62 is free\nX63 is free\nX162 is free\nX163 is free\ngopher(.(.(T115, T116), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(tail(.(T115, T116), X162), ','(tail(.(.(T115, T116), T104), X163), gopher(cons(T115, cons(X162, X163)), T92))), SCOPE: 45, CLAUSE: 5 | ','(tail(.(T115, T116), X162), ','(tail(.(.(T115, T116), T104), X163), gopher(cons(T115, cons(X162, X163)), T92))), SCOPE: 45, CLAUSE: 6\n\nT104 is ground\nT115 is ground\nT116 is ground\nX62 is free\nX63 is free\nX162 is free\nX163 is free\ngopher(.(.(T115, T116), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(tail(.(T115, T116), X162), ','(tail(.(.(T115, T116), T104), X163), gopher(cons(T115, cons(X162, X163)), T92))), SCOPE: 45, CLAUSE: 6\n\nT104 is ground\nT115 is ground\nT116 is ground\nX62 is free\nX63 is free\nX162 is free\nX163 is free\ngopher(.(.(T115, T116), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(tail(.(.(T121, T122), T104), X163), gopher(cons(T121, cons(T122, X163)), T92))\n\nT104 is ground\nT121 is ground\nT122 is ground\nX62 is free\nX63 is free\nX163 is free\ngopher(.(.(T121, T122), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(tail(.(.(T121, T122), T104), X163), gopher(cons(T121, cons(T122, X163)), T92)), SCOPE: 46, CLAUSE: 5 | ','(tail(.(.(T121, T122), T104), X163), gopher(cons(T121, cons(T122, X163)), T92)), SCOPE: 46, CLAUSE: 6\n\nT104 is ground\nT121 is ground\nT122 is ground\nX62 is free\nX63 is free\nX163 is free\ngopher(.(.(T121, T122), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(tail(.(.(T121, T122), T104), X163), gopher(cons(T121, cons(T122, X163)), T92)), SCOPE: 46, CLAUSE: 6\n\nT104 is ground\nT121 is ground\nT122 is ground\nX62 is free\nX63 is free\nX163 is free\ngopher(.(.(T121, T122), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: gopher(cons(T129, cons(T130, T131)), T92)\n\nT129 is ground\nT130 is ground\nT131 is ground\nX62 is free\nX63 is free\ngopher(.(.(T129, T130), T131), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 157 [arrowhead = none ];
157 -> 2;

158 [label="EVAL with clause\ngopher(nil, nil).\nand substitutionT1 -> nil,\nT2 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 158 [arrowhead = none ];
158 -> 3;

159 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
2 -> 159 [arrowhead = none ];
159 -> 4;

160 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 160 [arrowhead = none ];
160 -> 5;

161 [label="EVAL with clause\ngopher(X62, cons(nil, X63)) :- ','(no(empty(X62)), ','(head(X62, nil), tail(X62, X63))).\nand substitutionT1 -> T16,\nX62 -> T16,\nX63 -> T18,\nT2 -> cons(nil, T18),\nT17 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 161 [arrowhead = none ];
161 -> 46;

162 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 162 [arrowhead = none ];
162 -> 47;

163 [label="EVAL with clause\ngopher(X7, cons(nil, X8)) :- ','(no(empty(X7)), ','(head(X7, nil), tail(X7, X8))).\nand substitutionX7 -> nil,\nX8 -> T5,\nT2 -> cons(nil, T5),\nT4 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 163 [arrowhead = none ];
163 -> 6;

164 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 164 [arrowhead = none ];
164 -> 7;

165 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
6 -> 165 [arrowhead = none ];
165 -> 8;

166 [label="ONLY EVAL with clause\ngopher(X45, X46) :- ','(no(empty(X45)), ','(head(X45, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(X45, X50), gopher(cons(X48, cons(X49, X50)), X46))))))).\nand substitutionX45 -> nil,\nT2 -> T13,\nX46 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 166 [arrowhead = none ];
166 -> 34;

167 [label="ONLY EVAL with clause\nno(X11) :- ','(call(X11), ','(!_2, failure(a))).\nand substitutionX11 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 167 [arrowhead = none ];
167 -> 9;

168 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
9 -> 168 [arrowhead = none ];
168 -> 10;

169 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
10 -> 169 [arrowhead = none ];
169 -> 11;

170 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 170 [arrowhead = none ];
170 -> 12;

171 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 171 [arrowhead = none ];
171 -> 13;

172 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 172 [arrowhead = none ];
172 -> 14;

173 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 173 [arrowhead = none ];
173 -> 15;

174 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 174 [arrowhead = none ];
174 -> 16;

175 [label="ONLY EVAL with clause\nno(X16).\nand substitutionX16 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 175 [arrowhead = none ];
175 -> 17;

176 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 176 [arrowhead = none ];
176 -> 21;

177 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 177 [arrowhead = none ];
177 -> 18;

178 [label="BACKTRACK\nfor clause: head([], X1)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 178 [arrowhead = none ];
178 -> 19;

179 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 179 [arrowhead = none ];
179 -> 20;

180 [label="ONLY EVAL with clause\ngopher(X28, X29) :- ','(no(empty(X28)), ','(head(X28, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(X28, X33), gopher(cons(X31, cons(X32, X33)), X29))))))).\nand substitutionX28 -> nil,\nT2 -> T10,\nX29 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 180 [arrowhead = none ];
180 -> 22;

181 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 181 [arrowhead = none ];
181 -> 23;

182 [label="ONLY EVAL with clause\nno(X36) :- ','(call(X36), ','(!_6, failure(a))).\nand substitutionX36 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 182 [arrowhead = none ];
182 -> 24;

183 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
24 -> 183 [arrowhead = none ];
183 -> 25;

184 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
25 -> 184 [arrowhead = none ];
184 -> 26;

185 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 185 [arrowhead = none ];
185 -> 27;

186 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 186 [arrowhead = none ];
186 -> 28;

187 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 187 [arrowhead = none ];
187 -> 29;

188 [label="ONLY EVAL with clause\nno(X39).\nand substitutionX39 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 188 [arrowhead = none ];
188 -> 30;

189 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
30 -> 189 [arrowhead = none ];
189 -> 31;

190 [label="BACKTRACK\nfor clause: head([], X1)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 190 [arrowhead = none ];
190 -> 32;

191 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 191 [arrowhead = none ];
191 -> 33;

192 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
34 -> 192 [arrowhead = none ];
192 -> 35;

193 [label="ONLY EVAL with clause\nno(X53) :- ','(call(X53), ','(!_10, failure(a))).\nand substitutionX53 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 193 [arrowhead = none ];
193 -> 36;

194 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
36 -> 194 [arrowhead = none ];
194 -> 37;

195 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
37 -> 195 [arrowhead = none ];
195 -> 38;

196 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 196 [arrowhead = none ];
196 -> 39;

197 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 197 [arrowhead = none ];
197 -> 40;

198 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 198 [arrowhead = none ];
198 -> 41;

199 [label="ONLY EVAL with clause\nno(X56).\nand substitutionX56 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 199 [arrowhead = none ];
199 -> 42;

200 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
42 -> 200 [arrowhead = none ];
200 -> 43;

201 [label="BACKTRACK\nfor clause: head([], X1)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 201 [arrowhead = none ];
201 -> 44;

202 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 202 [arrowhead = none ];
202 -> 45;

203 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
46 -> 203 [arrowhead = none ];
203 -> 48;

204 [label="ONLY EVAL with clause\ngopher(X158, X159) :- ','(no(empty(X158)), ','(head(X158, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(X158, X163), gopher(cons(X161, cons(X162, X163)), X159))))))).\nand substitutionT1 -> T90,\nX158 -> T90,\nT2 -> T92,\nX159 -> T92,\nT91 -> T92", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 204 [arrowhead = none ];
204 -> 118;

205 [label="ONLY EVAL with clause\nno(X66) :- ','(call(X66), ','(!_14, failure(a))).\nand substitutionT16 -> T21,\nX66 -> empty(T21)", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 205 [arrowhead = none ];
205 -> 49;

206 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
49 -> 206 [arrowhead = none ];
206 -> 50;

207 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
50 -> 207 [arrowhead = none ];
207 -> 51;

208 [label="EVAL with clause\nempty([]).\nand substitutionT21 -> []", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 208 [arrowhead = none ];
208 -> 52;

209 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 209 [arrowhead = none ];
209 -> 53;

210 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 210 [arrowhead = none ];
210 -> 54;

211 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 211 [arrowhead = none ];
211 -> 68;

212 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 212 [arrowhead = none ];
212 -> 55;

213 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 213 [arrowhead = none ];
213 -> 56;

214 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
55 -> 214 [arrowhead = none ];
214 -> 57;

215 [label="ONLY EVAL with clause\ngopher(X75, X76) :- ','(no(empty(X75)), ','(head(X75, X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail(X75, X80), gopher(cons(X78, cons(X79, X80)), X76))))))).\nand substitutionX75 -> [],\nT2 -> T26,\nX76 -> T26,\nT25 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 215 [arrowhead = none ];
215 -> 59;

216 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 216 [arrowhead = none ];
216 -> 58;

217 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
59 -> 217 [arrowhead = none ];
217 -> 60;

218 [label="ONLY EVAL with clause\nno(X83) :- ','(call(X83), ','(!_18, failure(a))).\nand substitutionX83 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 218 [arrowhead = none ];
218 -> 61;

219 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
61 -> 219 [arrowhead = none ];
219 -> 62;

220 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
62 -> 220 [arrowhead = none ];
220 -> 63;

221 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 221 [arrowhead = none ];
221 -> 64;

222 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 222 [arrowhead = none ];
222 -> 65;

223 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
65 -> 223 [arrowhead = none ];
223 -> 66;

224 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 224 [arrowhead = none ];
224 -> 67;

225 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 225 [arrowhead = none ];
225 -> 69;

226 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
69 -> 226 [arrowhead = none ];
226 -> 70;

227 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
69 -> 227 [arrowhead = none ];
227 -> 71;

228 [label="ONLY EVAL with clause\nno(X88).\nand substitutionT21 -> T31,\nX88 -> empty(T31)", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 228 [arrowhead = none ];
228 -> 72;

229 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 229 [arrowhead = none ];
229 -> 82;

230 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
72 -> 230 [arrowhead = none ];
230 -> 73;

231 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T31), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 231 [arrowhead = none ];
231 -> 74;

232 [label="EVAL with clause\nhead(.(X94, X95), X94).\nand substitutionX94 -> nil,\nX95 -> T37,\nT31 -> .(nil, T37),\nT36 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 232 [arrowhead = none ];
232 -> 75;

233 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 233 [arrowhead = none ];
233 -> 76;

234 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
75 -> 234 [arrowhead = none ];
234 -> 77;

235 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 235 [arrowhead = none ];
235 -> 78;

236 [label="EVAL with clause\ntail(.(X100, X101), X101).\nand substitutionX100 -> nil,\nT37 -> T40,\nX101 -> T40,\nT18 -> T40", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 236 [arrowhead = none ];
236 -> 79;

237 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 237 [arrowhead = none ];
237 -> 80;

238 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 238 [arrowhead = none ];
238 -> 81;

239 [label="ONLY EVAL with clause\ngopher(X110, X111) :- ','(no(empty(X110)), ','(head(X110, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(X110, X115), gopher(cons(X113, cons(X114, X115)), X111))))))).\nand substitutionT21 -> T46,\nX110 -> T46,\nT2 -> T48,\nX111 -> T48,\nT47 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 239 [arrowhead = none ];
239 -> 83;

240 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
83 -> 240 [arrowhead = none ];
240 -> 84;

241 [label="ONLY EVAL with clause\nno(X118) :- ','(call(X118), ','(!_24, failure(a))).\nand substitutionT46 -> T51,\nX118 -> empty(T51)", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 241 [arrowhead = none ];
241 -> 85;

242 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
85 -> 242 [arrowhead = none ];
242 -> 86;

243 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
86 -> 243 [arrowhead = none ];
243 -> 87;

244 [label="BACKTRACK\nfor clause: empty([])\nwith clash: (empty(T51), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
87 -> 244 [arrowhead = none ];
244 -> 88;

245 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 245 [arrowhead = none ];
245 -> 89;

246 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 246 [arrowhead = none ];
246 -> 90;

247 [label="ONLY EVAL with clause\nno(X121).\nand substitutionT51 -> T54,\nX121 -> empty(T54)", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 247 [arrowhead = none ];
247 -> 91;

248 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
91 -> 248 [arrowhead = none ];
248 -> 92;

249 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T54), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
92 -> 249 [arrowhead = none ];
249 -> 93;

250 [label="EVAL with clause\nhead(.(X128, X129), X128).\nand substitutionX128 -> T59,\nX129 -> T60,\nT54 -> .(T59, T60),\nX112 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 250 [arrowhead = none ];
250 -> 94;

251 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 251 [arrowhead = none ];
251 -> 95;

252 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
94 -> 252 [arrowhead = none ];
252 -> 96;

253 [label="ONLY EVAL with clause\nno(X132) :- ','(call(X132), ','(!_28, failure(a))).\nand substitutionT59 -> T63,\nX132 -> empty(T63)", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 253 [arrowhead = none ];
253 -> 97;

254 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
97 -> 254 [arrowhead = none ];
254 -> 98;

255 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
98 -> 255 [arrowhead = none ];
255 -> 99;

256 [label="EVAL with clause\nempty([]).\nand substitutionT63 -> []", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 256 [arrowhead = none ];
256 -> 100;

257 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 257 [arrowhead = none ];
257 -> 101;

258 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 258 [arrowhead = none ];
258 -> 102;

259 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 259 [arrowhead = none ];
259 -> 105;

260 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
102 -> 260 [arrowhead = none ];
260 -> 103;

261 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 261 [arrowhead = none ];
261 -> 104;

262 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
105 -> 262 [arrowhead = none ];
262 -> 106;

263 [label="ONLY EVAL with clause\nno(X135).\nand substitutionT63 -> T66,\nX135 -> empty(T66)", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 263 [arrowhead = none ];
263 -> 107;

264 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
107 -> 264 [arrowhead = none ];
264 -> 108;

265 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T66), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 265 [arrowhead = none ];
265 -> 109;

266 [label="EVAL with clause\nhead(.(X142, X143), X142).\nand substitutionX142 -> T71,\nX143 -> T72,\nT66 -> .(T71, T72),\nX113 -> T71", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 266 [arrowhead = none ];
266 -> 110;

267 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 267 [arrowhead = none ];
267 -> 111;

268 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
110 -> 268 [arrowhead = none ];
268 -> 112;

269 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 269 [arrowhead = none ];
269 -> 113;

270 [label="ONLY EVAL with clause\ntail(.(X148, X149), X149).\nand substitutionT71 -> T77,\nX148 -> T77,\nT72 -> T78,\nX149 -> T78,\nX114 -> T78", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 270 [arrowhead = none ];
270 -> 114;

271 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
114 -> 271 [arrowhead = none ];
271 -> 115;

272 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 272 [arrowhead = none ];
272 -> 116;

273 [label="ONLY EVAL with clause\ntail(.(X154, X155), X155).\nand substitutionT77 -> T85,\nT78 -> T86,\nX154 -> .(T85, T86),\nT60 -> T87,\nX155 -> T87,\nX115 -> T87", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 273 [arrowhead = none ];
273 -> 117;

274 [label="INSTANCE with matching:\nT1 -> cons(T85, cons(T86, T87))\nT2 -> T48", fontsize=14, style = filled, fillcolor = lightgrey];
117 -> 274 [arrowhead = none , style=dashed];
274 -> 1[style=dashed];

275 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
118 -> 275 [arrowhead = none ];
275 -> 119;

276 [label="ONLY EVAL with clause\nno(X166) :- ','(call(X166), ','(!_35, failure(a))).\nand substitutionT90 -> T95,\nX166 -> empty(T95)", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 276 [arrowhead = none ];
276 -> 120;

277 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
120 -> 277 [arrowhead = none ];
277 -> 121;

278 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
121 -> 278 [arrowhead = none ];
278 -> 122;

279 [label="EVAL with clause\nempty([]).\nand substitutionT95 -> []", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 279 [arrowhead = none ];
279 -> 123;

280 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 280 [arrowhead = none ];
280 -> 124;

281 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 281 [arrowhead = none ];
281 -> 125;

282 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
124 -> 282 [arrowhead = none ];
282 -> 128;

283 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
125 -> 283 [arrowhead = none ];
283 -> 126;

284 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 284 [arrowhead = none ];
284 -> 127;

285 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 285 [arrowhead = none ];
285 -> 129;

286 [label="ONLY EVAL with clause\nno(X169).\nand substitutionT95 -> T98,\nX169 -> empty(T98)", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 286 [arrowhead = none ];
286 -> 130;

287 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
130 -> 287 [arrowhead = none ];
287 -> 131;

288 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T98), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
131 -> 288 [arrowhead = none ];
288 -> 132;

289 [label="EVAL with clause\nhead(.(X176, X177), X176).\nand substitutionX176 -> T103,\nX177 -> T104,\nT98 -> .(T103, T104),\nX160 -> T103", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 289 [arrowhead = none ];
289 -> 133;

290 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 290 [arrowhead = none ];
290 -> 134;

291 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
133 -> 291 [arrowhead = none ];
291 -> 135;

292 [label="ONLY EVAL with clause\nno(X180) :- ','(call(X180), ','(!_40, failure(a))).\nand substitutionT103 -> T107,\nX180 -> empty(T107)", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 292 [arrowhead = none ];
292 -> 136;

293 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
136 -> 293 [arrowhead = none ];
293 -> 137;

294 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
137 -> 294 [arrowhead = none ];
294 -> 138;

295 [label="EVAL with clause\nempty([]).\nand substitutionT107 -> []", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 295 [arrowhead = none ];
295 -> 139;

296 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 296 [arrowhead = none ];
296 -> 140;

297 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 297 [arrowhead = none ];
297 -> 141;

298 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 298 [arrowhead = none ];
298 -> 144;

299 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
141 -> 299 [arrowhead = none ];
299 -> 142;

300 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
142 -> 300 [arrowhead = none ];
300 -> 143;

301 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
144 -> 301 [arrowhead = none ];
301 -> 145;

302 [label="ONLY EVAL with clause\nno(X183).\nand substitutionT107 -> T110,\nX183 -> empty(T110)", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 302 [arrowhead = none ];
302 -> 146;

303 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
146 -> 303 [arrowhead = none ];
303 -> 147;

304 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T110), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 304 [arrowhead = none ];
304 -> 148;

305 [label="EVAL with clause\nhead(.(X190, X191), X190).\nand substitutionX190 -> T115,\nX191 -> T116,\nT110 -> .(T115, T116),\nX161 -> T115", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 305 [arrowhead = none ];
305 -> 149;

306 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 306 [arrowhead = none ];
306 -> 150;

307 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
149 -> 307 [arrowhead = none ];
307 -> 151;

308 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
151 -> 308 [arrowhead = none ];
308 -> 152;

309 [label="ONLY EVAL with clause\ntail(.(X196, X197), X197).\nand substitutionT115 -> T121,\nX196 -> T121,\nT116 -> T122,\nX197 -> T122,\nX162 -> T122", fontsize=14, style = filled, fillcolor = lightblue];
152 -> 309 [arrowhead = none ];
309 -> 153;

310 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
153 -> 310 [arrowhead = none ];
310 -> 154;

311 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 311 [arrowhead = none ];
311 -> 155;

312 [label="ONLY EVAL with clause\ntail(.(X202, X203), X203).\nand substitutionT121 -> T129,\nT122 -> T130,\nX202 -> .(T129, T130),\nT104 -> T131,\nX203 -> T131,\nX163 -> T131", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 312 [arrowhead = none ];
312 -> 156;

313 [label="INSTANCE with matching:\nT1 -> cons(T129, cons(T130, T131))\nT2 -> T92", fontsize=14, style = filled, fillcolor = lightgrey];
156 -> 313 [arrowhead = none , style=dashed];
313 -> 1[style=dashed];

}

(2) Obligation:

Clauses:

gopherA(nil, nil).
gopherA(.(nil, T40), cons(nil, T40)).
gopherA(.(.(T85, T86), T87), T48) :- gopherA(cons(T85, cons(T86, T87)), T48).
gopherA(.(.(T129, T130), T131), T92) :- gopherA(cons(T129, cons(T130, T131)), T92).

Query: gopherA(g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
gopherA_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(.(nil, T40), cons(nil, T40)) → gopherA_out_ga(.(nil, T40), cons(nil, T40))
gopherA_in_ga(.(.(T85, T86), T87), T48) → U1_ga(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
gopherA_in_ga(.(.(T129, T130), T131), T92) → U2_ga(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))
U2_ga(T129, T130, T131, T92, gopherA_out_ga(cons(T129, cons(T130, T131)), T92)) → gopherA_out_ga(.(.(T129, T130), T131), T92)
U1_ga(T85, T86, T87, T48, gopherA_out_ga(cons(T85, cons(T86, T87)), T48)) → gopherA_out_ga(.(.(T85, T86), T87), T48)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(.(nil, T40), cons(nil, T40)) → gopherA_out_ga(.(nil, T40), cons(nil, T40))
gopherA_in_ga(.(.(T85, T86), T87), T48) → U1_ga(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
gopherA_in_ga(.(.(T129, T130), T131), T92) → U2_ga(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))
U2_ga(T129, T130, T131, T92, gopherA_out_ga(cons(T129, cons(T130, T131)), T92)) → gopherA_out_ga(.(.(T129, T130), T131), T92)
U1_ga(T85, T86, T87, T48, gopherA_out_ga(cons(T85, cons(T86, T87)), T48)) → gopherA_out_ga(.(.(T85, T86), T87), T48)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

GOPHERA_IN_GA(.(.(T85, T86), T87), T48) → U1_GA(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
GOPHERA_IN_GA(.(.(T85, T86), T87), T48) → GOPHERA_IN_GA(cons(T85, cons(T86, T87)), T48)
GOPHERA_IN_GA(.(.(T129, T130), T131), T92) → U2_GA(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))

The TRS R consists of the following rules:

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(.(nil, T40), cons(nil, T40)) → gopherA_out_ga(.(nil, T40), cons(nil, T40))
gopherA_in_ga(.(.(T85, T86), T87), T48) → U1_ga(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
gopherA_in_ga(.(.(T129, T130), T131), T92) → U2_ga(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))
U2_ga(T129, T130, T131, T92, gopherA_out_ga(cons(T129, cons(T130, T131)), T92)) → gopherA_out_ga(.(.(T129, T130), T131), T92)
U1_ga(T85, T86, T87, T48, gopherA_out_ga(cons(T85, cons(T86, T87)), T48)) → gopherA_out_ga(.(.(T85, T86), T87), T48)

The argument filtering Pi contains the following mapping:
gopherA_in_ga(x1, x2) = gopherA_in_ga(x1)
nil = nil
gopherA_out_ga(x1, x2) = gopherA_out_ga(x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x5)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x5)
cons(x1, x2) = cons(x1, x2)
GOPHERA_IN_GA(x1, x2) = GOPHERA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x5)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x5)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules: